@CohenCyril, is a big-enough for finmap (as in the xfinmap.v file in this repo.) is now available? This would allow the removal of xfinmap.v

@hivert, I don't have any comment, although I would prefer to get rid of xfinmap.v before doing a merge.

The code is now ready for review/merging now. One question: the code now depends on finmap 1.1 which is not the version distributed with with opam. Is there any simple workflow which allows to have both switching when needed ?

Hi @hivert, both finmap 1.0.0 and 1.1.0 should be released though...

@CohenCyril, in which repository ? I can't find it in coq-core-dev, coq-released & coq-extra-dev.

If it's not obvious, travis failing is due to the use of finmap 1.0 and not finmap 1.1

https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.1.0

@CohenCyril, arg sorry, my opam remotes point to local git clone :)

If it's not obvious, travis failing is due to the use of finmap 1.0 and not finmap 1.1

Then you should update the version of finmap used by travis.... oh... but then both freeg and mpoly will stop working...

Well, that's not a problem per se as I'm currently pruning both files.

@hivert, could you change the opam file s.t. the dependencies are correct?

Or could you give me access to that PR (the option should be on the right "allow commits from maintainers")

@strub. The option was already checked, so you should have access. I'm in the middle of writing deliverable reports for some European project (https://opendreamkit.org/ if you are curious) which are due tomorrow evening so I won't have time for this PR until the week end. So please do any fix if you want.

@CohenCyril, is a big-enough for finmap (as in the xfinmap.v file in this repo.) is now available? This would allow the removal of xfinmap.v

not yet, please consider pushing it to finmap 1.1.0 master

@strub I'm very happy you merged this PR so quickly. I hope nothing was overlooked. My next step is to go to point 2 of #19 and contribute the general theory of linear function of a {malg R[M]} where M is just an choiceType and not yet a monoid... But not today ;-)

Be warned that I'm currently pruning mpoly.v, rebasing everything on top of malg.v and moving the M of R[M] up in the hierarchy when importing lemmas. It is likely that I won't be able to accept PR during this phase. As long as you are only developing a new theory, you should be fine. But any PR modifying current results of malg.v will be hardly mergeable after my commit.

@strub Don't you want to merge #15 first then?

I'm not sure what you mean by "moving the M of R[M] up in the hierarchy when importing lemmas". The theory I'd like to add is the following:

Consider some A := {malg R[M]} where M is just a choiceType and not yet a Monoid. Any function M -> A is uniquely and naturally extended by linearity to a function A -> A. The obtained function is of course canonically linear. This also works for maps M -> {malg R[N]} with two different support but the same ring. Iterating the construction leads to bilinear function which ultimately you can use to define the product when M is a monoid. Se the first section called MakeLinear in this file for more details.

To summarize: my point is: dealing with linearity can be done even one level up (M : choiceType) than with the current current code (M: Monoid). And I need this level of generality.

Is there any conflict between that plan and 'moving the M up' ?

Consider some A := {malg R[M]} where M is just a choiceType and not yet a Monoid. Any function M -> A is uniquely and naturally extended by linearity to a function A -> A.

Actually, unless I'm mistaken, any monoid morphism M -> B (where B is any R-algebra) is naturally isomorphic to an algebra map {malg R[M]} -> B, and that's how one should get both maps you (@hivert) described, and polynomial evaluation.

(PS1: By the way, I guess the following also works: for any ring morphism f : R -> R', any monoid morphism M -> B (where B is a R' algebra) is naturally ismorphic to an algebra map {malg R[M]} -> B)

(PS2: does this generalizes to a regular function M -> B where B is a Z-module and M a choiceType? do we get an additive map {alg R[M]} -> B?)

@CohenCyril, good point, I'm going to merge #15.

@hivert, by "up", I simply mean than I'll take the more general structure for "M" (stopping at "M" is a monoid). A very large part of the development only uses that M is a monoid/finite monoid/ordered monoid. This is why I'm choosing this step to prune mpoly.v. When done, as I wrote in my first message, I'm going to release the result (I have other people depending on that library, I'd like to provide them a clean version of what is actually in the repository). Then, we can all move to bigger changes without fearing gigantic conflicts.

@CohenCyril: good point (starting from a monoid morphism). I was more talking about your PS2 whose correct version seems to me the following universal property:

Given any ring R (which might be Z), for any plain map f:M -> B (where M is a choiceType and B is an R-module) there is a unique R-linear map linf:{malg R[M]} -> B such that linf <m> = f m (where <m> is the injection of m in {malg R[M]}). That is to say {malg R[M]} is the free R module generated by M.

I should have written that from the beginning in my code and this discussion.

By the way mathcomp hierarchy might force us to do the job twice: once for Z giving additive map and once for the other ring (linear maps).

@strub Ok ! I'll go on with my experiment but refrain changing the main files.

Given any ring R (which might be Z), for any plain map f:M -> B (where M is a choiceType and B is an R-module) there is a unique R-linear map linf:{malg R[M]} -> B such that linf = f m (where is the injection of m in {malg R[M]}). That is to say {malg R[M]} is the free R module generated by M.

Isn't that the composition of the two functions I describe in issue #19 (#19 (comment))

By the way mathcomp hierarchy might force us to do the job twice: once for Z giving additive map and once for the other ring (linear maps).

You may be right, I do not see how to factor those two :(

BTW I tried to fuel #19 instead of the thread of this merged PR (mea culpa)

@CohenCyril Good idea to stop discussing here since the PR is closed. Switching to #19